$\forall$$T$:Type, $x$:$T$, $L$, $L_{1}$, $L_{2}$:$T$ List.
\\[0ex]interleaving($T$;$L_{1}$;$L_{2}$;$x$.$L$)
\\[0ex]$\Leftrightarrow$
\\[0ex]0$<\parallel$$L_{1}$$\parallel$ \& $L_{1}$[0] $=$ $x$ \& interleaving($T$;tl($L_{1}$);$L_{2}$;$L$)
\\[0ex]$\vee$ 0$<\parallel$$L_{2}$$\parallel$ \& $L_{2}$[0] $=$ $x$ \& interleaving($T$;$L_{1}$;tl($L_{2}$);$L$)